perm filename REM[ESS,JMC] blob sn#016781 filedate 1972-12-08 generic text, type T, neo UTF8
(ADDAXIOM TRI
 ((FORALL X) ((FORALL Y) (OR (LESSP X Y) (LESSP Y X) (EQUAL X Y)))))

(ADDAXIOM TRI1
 ((FORALL X) ((FORALL Y) (NOT (AND (LESSP X Y) (LESSP Y X))))))

(ADDAXIOM TRI2
 ((FORALL X) ((FORALL Y) (NOT (AND (EQUAL X Y) (LESSP Y X))))))

(ADDAXIOM TRI3
 ((FORALL X) ((FORALL Y) (NOT (AND (EQUAL X Y) (LESSP X Y))))))

(ADDAXIOM EVOD ((FORALL X) (EQUIVALENT (EVEN X) (NOT (ODD X)))))

(ADDAXIOM EXOY
 ((FORALL X) (IMPLIES (AND (EVEN X) (ODD Y)) (NOT (EQUAL X Y)))))

(GIVEPROOF ONE
 ((1 (OR (LESSP A B) (LESSP B A) (EQUAL A B)) (USEAX TRI A B) NIL)
  (2 (OR (LESSP B A) (LESSP A B) (EQUAL B A)) (USEAX TRI B A) NIL)
  (3 (NOT (AND (LESSP A B) (LESSP B A))) (USEAX TRI1 A B) NIL)
  (4 (NOT (AND (LESSP B A) (LESSP A B))) (USEAX TRI1 B A) NIL)
  (5 (NOT (AND (EQUAL B A) (LESSP A B))) (USEAX TRI2 B A) NIL)
  (6 (NOT (AND (EQUAL A B) (LESSP B A))) (USEAX TRI2 A B) NIL)
  (7 (NOT (AND (EQUAL A B) (LESSP A B))) (USEAX TRI3 A B) NIL)
  (8 (NOT (AND (EQUAL B A) (LESSP B A))) (USEAX TRI3 B A) NIL)
  (9 (EQUIVALENT (EVEN A) (NOT (ODD A))) (USEAX EVOD A) NIL)
  (10 (EQUIVALENT (EVEN B) (NOT (ODD B))) (USEAX EVOD B) NIL)
  (11 (IMPLIES (AND (EVEN B) (ODD Y)) (NOT (EQUAL B Y)))
      (USEAX EXOY B)
      NIL)
  (12 (IMPLIES (AND (EVEN A) (ODD Y)) (NOT (EQUAL A Y)))
      (USEAX EXOY A)
      NIL)))